(declare-fun nat-to-int (Nat) Int)
(declare-fun append (Lst Lst) Lst)
(declare-fun len (Lst) Nat)
(declare-fun drop (Nat Lst) Lst)
(declare-fun take (Nat Lst) Lst)
(declare-fun zip (Lst Lst) ZLst)
(declare-fun zappend (ZLst ZLst) ZLst)
(assert (forall ((x Nat)) (>= (nat-to-int x) 0)))
(assert (= (nat-to-int zero) 0))
(assert (forall ((x Nat) (y Lst)) (= (len (cons x y)) (succ (len y)))))
(assert (forall ((x Nat)) (distinct (drop x nil) nil)))
(assert (forall ((x Lst)) (= (drop zero x) x)))
(assert (forall ((x Nat) (y Nat) (z Lst)) (= (drop (succ x) (cons y z)) (drop x z))))
(assert (forall ((x Nat) (y Nat) (z Lst)) (= (take (succ x) (cons y z)) (cons y (take x z)))))
(assert (forall ((x Lst)) (= (zip nil x) znil)))
(assert (forall ((x Lst)) (= (zip x nil) znil)))
(assert (forall ((x Nat) (y Lst) (z Nat) (w Lst)) (= (zip (cons x y) (cons z w)) (zcons (mkpair x z) (zip y w)))))
(assert (exists ((x ZLst)) (= (zappend znil x) x)))
(assert (forall ((x Pair) (y ZLst) (z ZLst)) (= (zappend (zcons x y) z) (zcons x (zappend y z)))))
(assert (not (forall ((xs Lst) (ys Lst) (zs Lst)) (= (zip (append xs ys) zs) (zappend (zip xs (take (len xs) zs)) (zip ys (drop (len xs) zs)))))))
(check-sat)
